4.2 Parallel Verification

4.2 Parallel Verification

Rapid development in hardware industry has brought the prevalence of multi-core systems with shared-memory, which enabled the speedup of various tasks by using parallel algorithms. The Linear Temporal Logic (LTL) model checking problem is one of the difficult problems to be parallelized or scaled up to multi-core. The research in parallelism of model checking fairness enhanced systems emits two challenges: Firstly, efficient parallel solution of many problems may result in dramatically different approaches from those to solve the same problems sequentially. Second, fairness, which is concerned with a fair resolution of non-determinism, is often important but expensive to be combined with existing parallel model checking algorithms.

In PAT, we successfully implemented a parallel model checking algorithm which is proposed in our paper [LIUSD09], with the capacity of parallel verification of systems with various fairness constraints in the multi-core architecture with share-memory. This algorithm is baesd on Tarjan's strongly connected components (SCC) detection algorithm, while extends it to parallel execution when multi-core environment is available. This algorithm is able to separate search space into smaller, independent searching spaces which natrually exclude each other, which allows the tasks of examinating each smaller seaching space to be scattered into free CPUs such that high concurrency and efficiency can be reached. Our parallel algorithm is quite acceptable with the linear(in the size of state space) time complexity.

As PAT integrated this parallel algorithm to achieve higher effinciency than sequantial execution, so when you have a Linear Temporal Logic(LTL) fomula to check, and happen to have a multi-core machine, you can simply check the "parallel verification" in the Verifier panel (refer to PAT Verifier, Parallel Verificaion) to use this parallel method. We also show the significant improvement by showing a comparison between checking a LTL property under certain fairness of the same model with and without choosing parallel execution.

Use the reader and writer's example (Descriptions refer to PAT Examples-> Classic Algorithms(CSP)) as an example. We choose number of processes to be 10 and the to-be-checked LTL property as eventually always there is one and only one leader in the network, under process level strong fairness.

#assert ReadersWriters() |= []<>error;

The result with 'parallel verification' is shown as follows:

********Verification Result********
The Assertion is NOT valid.
A counterexample is presented as follows.
<init -> (startwrite -> stopwrite -> startread -> startread -> startread -> startread -> startread -> startread -> startread -> startread -> startread -> startread -> stopread -> stopread -> stopread -> stopread -> stopread -> stopread -> stopread -> stopread -> stopread -> stopread -> startwrite)*>

Verification Statistics for un-parallelled verification is:

********Verification Statistics********
Visited States:27
Total Transitions:52
Time Used:0.1031619s
Estimated Memory Used:59411.476KB

Verification Statistics for parallel verification is:

********Verification Statistics********
Visited States:27
Total Transitions:52
Number of SCC found: 1
Total SCC states: 22
Average SCC Size: 22
SCC Ratio: 0.81
Time Used:0.0155166s
Estimated Memory Used:82917.568KB

This example shows that under such fairness restriction, the paralleled verification is faster than the un-parallelled one. You can also check other fairness properties like process level weak fairness, strong fairness etc. using parallelled method to speed-up verification.